\begin{tabbing}
$\forall$$k$:Knd, $T$, $A$, $B$:Type, $l$:IdLnk, $x$, ${\it tg}$:Id, $f$:($A$$\rightarrow$$B$$\rightarrow$$T$), $c$:($A$$\rightarrow$$B$$\rightarrow\mathbb{B}$), ${\it es}$:ES.
\\[0ex]sends1{-}p(${\it es}$;$x$;$A$;$k$;$B$;$l$;${\it tg}$;$T$;$\lambda$$a$,$b$. if $c$($a$,$b$) then [($f$($a$,$b$))] else [] fi )
\\[0ex]$\Rightarrow$  $k$\=(v:$B$) sends\+
\\[0ex]$f$($x$:$A$,v) on
\\[0ex]$l$ tagged with ${\it tg}$:$T$
\\[0ex]provided $c$($x$,v)
\-
\end{tabbing}